ds:x:Id fp Type, da:k:Knd fp Type, m:, A:ecl-trans-tuple{i:l}(ds;da).
add-ecl-act(A;m)  ecl-trans-tuple{i:l}(ds;da) 

latex

Definitions	t  T, x:A. B(x), AB, P  Q, False, A, , , , Valtype(da;k), State(ds), Knd, (x  l), false, p  q, reduce(f;k;as), b, p  q, i=j, if b t else f fi, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), add-ecl-act(A;m), ecl-trans-tuple{i:l}(ds;da), Id, x. t(x), a:A fp B(a)
Lemmas	ecl-trans-tuple wf, fpf wf, Id wf, ifthenelse wf, eq int wf, band wf, bnot wf, reduce wf, bor wf, nat plus inc, bfalse wf, nat wf, l member wf, Knd wf, decl-state wf, ma-valtype wf, bool wf, nat plus wf, le wf